The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for tracking array data contents across three-valued read and write operations.
Modern chip designs are complex and often involve arrays, a basic memory block that contains a set of data words. One can characterize an array by the number of bits in the data address and the number of bits in each data word. Arrays support the primitive operations of write (address, data), which is used to update the array contents, and read (address), which is used to fetch data from the array.
Applications, such as simulation and formal verification, often use non-determinism. One may use non-determinism to either make the model more general or to alleviate performance problems. Typically, each signal has a binary value of 0 (zero) or 1 (one). Non-determinism introduces the new symbol, X, which means that the value of a signal is not known. This X symbol represents a non-determined value. This formulation is often called ternary, or three-valued, modeling.
Ternary modeling becomes problematic when a design has arrays. Suppose one performs a read at an address that contains X symbols. This means that certain bits of the address are unknown and could take either the value of 0 or 1. In effect, the address could resolve to one of a set of possible concrete (X-free) addresses, and the number of concrete addresses is equal to 2N, where N is the number of bits in the address with an X value. Essentially, this means that one no longer knows which address is being read from. For writes, one may not know the exact write address, and one also may not know the exact value being written.
For designs with arrays, simulators often take lossy shortcuts. For example, a simulator may consider the entire array to have value X if any X appears on any write address, or it may raise an exception if an X appears in the address.
Additionally, a design model includes an enable signal that is paired with each read and write operation. A read enable signal specifies whether the read actually reads from the array or merely returns random values. A write enable signal specifies whether the array should actually be updated. It is possible for X values to appear on enable signals. In the case of an X on a write enable signal, the array contents can be difficult to model. Existing simulators take shortcuts, often settling the entire array contents to X in such cases or raising an exception. While this approximation is sound because the approximated data is a superset of the real data, such a shortcut loses much of the precision.
The raise-exception approach outright precludes the use of performing ternary simulation for many practically useful design and verification tasks. For example, three-valued simulation is often an all-X state. Similarly, numerous pervasive logic verification tasks, such as “fencing logic verification,” require ternary simulation to access whether an X value may propagate beyond some logical boundary. Such simulator shortcuts result in very coarse approximations or outright preclude the use of ternary simulators for such applications on designs with memory arrays.